Nuprl Definition : ma-interface-glued-p 11,40

ma-interface-glued-p(es;A;I;l;tg)
== ma-interface-consistent(es;I)
== & (e:E. (kind(e) = rcv(l,tg))  (valtype(e) r A))
== & glued(es; A; (e.[[I]](e)); [[I]]; es-in-port(es;l;tg)) 
latex



clarification:

ma-interface-glued-p(es;A;I;l;tg)
== ma-interface-consistent(es;I)
== & (e:es-E(es). (es-kind(es; e) = rcv(l,tg)  Knd)  (es-valtype(es; e) r A))
== & glued(es; A; (e.ma-abs-interface(es;I)(e)); ma-abs-interface(es;I); es-in-port(es;l;tg)) 
latex


Definitionsma-interface-consistent(es;X), P & Q, x:A. B(x), E, P  Q, s = t, Knd, kind(e), rcv(l,tg), valtype(e), glued(es; B; f; Ia; Ib), x.A(x), X(e), [[X]], es-in-port(es;l;tg)
FDL editor aliasesma-interface-glued-p

origin